Promela の do
if
とほぼ同じ構文
無限ループを作る
break
で脱出できる